<!DOCTYPE html>
<html lang="zh-CN">
<head>
  <meta charset="UTF-8">
<meta name="viewport" content="width=device-width">
<meta name="theme-color" content="#222"><meta name="generator" content="Hexo 6.3.0">

  <link rel="apple-touch-icon" sizes="180x180" href="/blog/images/apple-touch-icon-next.png">
  <link rel="icon" type="image/png" sizes="32x32" href="/blog/images/Horse.png">
  <link rel="icon" type="image/png" sizes="16x16" href="/blog/images/Horse.png">
  <link rel="mask-icon" href="/blog/images/logo.svg" color="#222">

<link rel="stylesheet" href="/blog/css/main.css">



<link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/font-awesome/6.4.0/css/all.min.css" integrity="sha256-HtsXJanqjKTc8vVQjO4YMhiqFoXkfBsjBWcX91T1jr8=" crossorigin="anonymous">
  <link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/fancybox/3.5.7/jquery.fancybox.min.css" integrity="sha256-Vzbj7sDDS/woiFS3uNKo8eIuni59rjyNGtXfstRzStA=" crossorigin="anonymous">

<script class="next-config" data-name="main" type="application/json">{"hostname":"yanlwsometing.gitee.io","root":"/blog/","images":"/blog/images","scheme":"Pisces","darkmode":false,"version":"8.16.0","exturl":false,"sidebar":{"position":"left","display":"post","padding":18,"offset":12},"copycode":{"enable":true,"show_result":true,"style":"flat"},"bookmark":{"enable":false,"color":"#222","save":"auto"},"mediumzoom":false,"lazyload":false,"pangu":false,"comments":{"style":"tabs","active":null,"storage":true,"lazyload":false,"nav":null},"stickytabs":false,"motion":{"enable":false,"async":false,"transition":{"menu_item":"fadeInDown","post_block":"fadeIn","post_header":"fadeInDown","post_body":"fadeInDown","coll_header":"fadeInLeft","sidebar":"fadeInUp"}},"prism":false,"i18n":{"placeholder":"搜索...","empty":"没有找到任何搜索结果：${query}","hits_time":"找到 ${hits} 个搜索结果（用时 ${time} 毫秒）","hits":"找到 ${hits} 个搜索结果"}}</script><script src="/blog/js/config.js"></script>

    <meta name="description" content="数值序对(Pairs of Numbers)在 Inductive 类型定义中，每个构造子（Constructor）可以有任意多个参数 —— 可以没有（如 true 和 O），可以只有一个（如 S），也可以更多 （如 nybble，以及下文所示）。 1. 定义本文中创建了一种携带两个参数的类型，并为其声明操作函数和记法： 12345678910111213141516171819202122232">
<meta property="og:type" content="article">
<meta property="og:title" content="SF-1-Lists">
<meta property="og:url" content="https://yanlwsometing.gitee.io/blog/2023/07/18/SF-1-Lists/index.html">
<meta property="og:site_name" content="yanlwsometing">
<meta property="og:description" content="数值序对(Pairs of Numbers)在 Inductive 类型定义中，每个构造子（Constructor）可以有任意多个参数 —— 可以没有（如 true 和 O），可以只有一个（如 S），也可以更多 （如 nybble，以及下文所示）。 1. 定义本文中创建了一种携带两个参数的类型，并为其声明操作函数和记法： 12345678910111213141516171819202122232">
<meta property="og:locale" content="zh_CN">
<meta property="article:published_time" content="2023-07-18T14:44:44.000Z">
<meta property="article:modified_time" content="2023-12-15T09:08:29.955Z">
<meta property="article:author" content="yanlw">
<meta property="article:tag" content="博客">
<meta name="twitter:card" content="summary">


<link rel="canonical" href="https://yanlwsometing.gitee.io/blog/2023/07/18/SF-1-Lists/">



<script class="next-config" data-name="page" type="application/json">{"sidebar":"","isHome":false,"isPost":true,"lang":"zh-CN","comments":true,"permalink":"https://yanlwsometing.gitee.io/blog/2023/07/18/SF-1-Lists/","path":"2023/07/18/SF-1-Lists/","title":"SF-1-Lists"}</script>

<script class="next-config" data-name="calendar" type="application/json">""</script>
<title>SF-1-Lists | yanlwsometing</title>
  








  <noscript>
    <link rel="stylesheet" href="/blog/css/noscript.css">
  </noscript>
</head>

<body itemscope itemtype="http://schema.org/WebPage">
  <div class="headband"></div>

  <main class="main">
    <div class="column">
      <header class="header" itemscope itemtype="http://schema.org/WPHeader"><div class="site-brand-container">
  <div class="site-nav-toggle">
    <div class="toggle" aria-label="切换导航栏" role="button">
        <span class="toggle-line"></span>
        <span class="toggle-line"></span>
        <span class="toggle-line"></span>
    </div>
  </div>

  <div class="site-meta">

    <a href="/blog/" class="brand" rel="start">
      <i class="logo-line"></i>
      <p class="site-title">yanlwsometing</p>
      <i class="logo-line"></i>
    </a>
  </div>

  <div class="site-nav-right">
    <div class="toggle popup-trigger" aria-label="搜索" role="button">
    </div>
  </div>
</div>



<nav class="site-nav">
  <ul class="main-menu menu"><li class="menu-item menu-item-home"><a href="/blog/" rel="section"><i class="fa fa-home fa-fw"></i>首页</a></li><li class="menu-item menu-item-tags"><a href="/blog/tags/" rel="section"><i class="fa fa-tags fa-fw"></i>标签</a></li><li class="menu-item menu-item-categories"><a href="/blog/categories/" rel="section"><i class="fa fa-th fa-fw"></i>分类</a></li><li class="menu-item menu-item-archives"><a href="/blog/archives/" rel="section"><i class="fa fa-archive fa-fw"></i>归档</a></li><li class="menu-item menu-item-commonweal"><a href="/blog/404/" rel="section"><i class="fa fa-heartbeat fa-fw"></i>公益 404</a></li>
  </ul>
</nav>




</header>
        
  
  <aside class="sidebar">

    <div class="sidebar-inner sidebar-nav-active sidebar-toc-active">
      <ul class="sidebar-nav">
        <li class="sidebar-nav-toc">
          文章目录
        </li>
        <li class="sidebar-nav-overview">
          站点概览
        </li>
      </ul>

      <div class="sidebar-panel-container">
        <!--noindex-->
        <div class="post-toc-wrap sidebar-panel">
            <div class="post-toc animated"><ol class="nav"><li class="nav-item nav-level-2"><a class="nav-link" href="#%E6%95%B0%E5%80%BC%E5%BA%8F%E5%AF%B9-Pairs-of-Numbers"><span class="nav-number">1.</span> <span class="nav-text">数值序对(Pairs of Numbers)</span></a><ol class="nav-child"><li class="nav-item nav-level-3"><a class="nav-link" href="#1-%E5%AE%9A%E4%B9%89"><span class="nav-number">1.1.</span> <span class="nav-text">1. 定义</span></a></li><li class="nav-item nav-level-3"><a class="nav-link" href="#2-match-p-vs-match-n-m"><span class="nav-number">1.2.</span> <span class="nav-text">2. match p vs. match n,m</span></a></li><li class="nav-item nav-level-3"><a class="nav-link" href="#3-%E5%BA%8F%E5%AF%B9%E7%9A%84%E7%AE%80%E5%8D%95%E8%AF%81%E6%98%8E"><span class="nav-number">1.3.</span> <span class="nav-text">3. 序对的简单证明</span></a></li></ol></li><li class="nav-item nav-level-2"><a class="nav-link" href="#%E6%95%B0%E5%80%BC%E5%88%97%E8%A1%A8-Lists-of-Numbers"><span class="nav-number">2.</span> <span class="nav-text">数值列表(Lists of Numbers)</span></a><ol class="nav-child"><li class="nav-item nav-level-3"><a class="nav-link" href="#1-%E5%AE%9A%E4%B9%89-1"><span class="nav-number">2.1.</span> <span class="nav-text">1. 定义</span></a></li><li class="nav-item nav-level-3"><a class="nav-link" href="#2-%E7%94%A8%E5%88%97%E8%A1%A8%E5%AE%9E%E7%8E%B0%E5%8F%A3%E8%A2%8B%EF%BC%88Bag%EF%BC%89"><span class="nav-number">2.2.</span> <span class="nav-text">2. 用列表实现口袋（Bag）</span></a></li></ol></li><li class="nav-item nav-level-2"><a class="nav-link" href="#%E6%9C%89%E5%85%B3%E5%88%97%E8%A1%A8%E7%9A%84%E8%AE%BA%E8%AF%81-Reasoning-About-Lists"><span class="nav-number">3.</span> <span class="nav-text">有关列表的论证(Reasoning About Lists)</span></a><ol class="nav-child"><li class="nav-item nav-level-3"><a class="nav-link" href="#1-%E5%AF%B9%E5%88%97%E8%A1%A8%E5%BD%92%E7%BA%B3-Induction-on-Lists"><span class="nav-number">3.1.</span> <span class="nav-text">1. 对列表归纳(Induction on Lists)</span></a></li><li class="nav-item nav-level-3"><a class="nav-link" href="#2-%E5%8F%8D%E8%BD%AC%E5%88%97%E8%A1%A8-Reversing-a-List"><span class="nav-number">3.2.</span> <span class="nav-text">2. 反转列表(Reversing a List )</span></a></li><li class="nav-item nav-level-3"><a class="nav-link" href="#3-Search"><span class="nav-number">3.3.</span> <span class="nav-text">3.  Search</span></a></li></ol></li><li class="nav-item nav-level-2"><a class="nav-link" href="#Options-%E5%8F%AF%E9%80%89%E7%B1%BB%E5%9E%8B"><span class="nav-number">4.</span> <span class="nav-text">Options 可选类型</span></a></li><li class="nav-item nav-level-2"><a class="nav-link" href="#%E5%81%8F%E6%98%A0%E5%B0%84-%EF%BC%88Partial-Maps%EF%BC%89"><span class="nav-number">5.</span> <span class="nav-text">偏映射 （Partial Maps）</span></a></li><li class="nav-item nav-level-2"><a class="nav-link" href="#Exercises"><span class="nav-number">6.</span> <span class="nav-text">Exercises</span></a></li></ol></div>
        </div>
        <!--/noindex-->

        <div class="site-overview-wrap sidebar-panel">
          <div class="site-author animated" itemprop="author" itemscope itemtype="http://schema.org/Person">
    <img class="site-author-image" itemprop="image" alt="yanlw"
      src="/blog/images/avatar.jpg">
  <p class="site-author-name" itemprop="name">yanlw</p>
  <div class="site-description" itemprop="description">穷则独善其身，达则兼济天下！</div>
</div>
<div class="site-state-wrap animated">
  <nav class="site-state">
      <div class="site-state-item site-state-posts">
        <a href="/blog/archives/">
          <span class="site-state-item-count">23</span>
          <span class="site-state-item-name">日志</span>
        </a>
      </div>
      <div class="site-state-item site-state-categories">
          <a href="/blog/categories/">
        <span class="site-state-item-count">9</span>
        <span class="site-state-item-name">分类</span></a>
      </div>
      <div class="site-state-item site-state-tags">
          <a href="/blog/tags/">
        <span class="site-state-item-count">18</span>
        <span class="site-state-item-name">标签</span></a>
      </div>
  </nav>
</div>
  <div class="links-of-author animated">
      <span class="links-of-author-item">
        <a href="https://gitee.com/yanlwsometing" title="Gitee → https:&#x2F;&#x2F;gitee.com&#x2F;yanlwsometing" rel="noopener me" target="_blank"><i class="fab fa-gitee fa-fw"></i>Gitee</a>
      </span>
      <span class="links-of-author-item">
        <a href="mailto:1977712019@qq.com" title="Mail → mailto:1977712019@qq.com" rel="noopener me" target="_blank"><i class="fa fa-envelope fa-fw"></i>Mail</a>
      </span>
      <span class="links-of-author-item">
        <a href="https://weibo.com/" title="Weibo → https:&#x2F;&#x2F;weibo.com&#x2F;" rel="noopener me" target="_blank"><i class="fab fa-weibo fa-fw"></i>Weibo</a>
      </span>
      <span class="links-of-author-item">
        <a href="https://twitter.com/" title="Twitter → https:&#x2F;&#x2F;twitter.com&#x2F;" rel="noopener me" target="_blank"><i class="fab fa-twitter fa-fw"></i>Twitter</a>
      </span>
  </div>

        </div>
      </div>
        <div class="back-to-top animated" role="button" aria-label="返回顶部">
          <i class="fa fa-arrow-up"></i>
          <span>0%</span>
        </div>
    </div>

    
  </aside>


    </div>

    <div class="main-inner post posts-expand">


  


<div class="post-block">
  
  

  <article itemscope itemtype="http://schema.org/Article" class="post-content" lang="zh-CN">
    <link itemprop="mainEntityOfPage" href="https://yanlwsometing.gitee.io/blog/2023/07/18/SF-1-Lists/">

    <span hidden itemprop="author" itemscope itemtype="http://schema.org/Person">
      <meta itemprop="image" content="/blog/images/avatar.jpg">
      <meta itemprop="name" content="yanlw">
    </span>

    <span hidden itemprop="publisher" itemscope itemtype="http://schema.org/Organization">
      <meta itemprop="name" content="yanlwsometing">
      <meta itemprop="description" content="穷则独善其身，达则兼济天下！">
    </span>

    <span hidden itemprop="post" itemscope itemtype="http://schema.org/CreativeWork">
      <meta itemprop="name" content="SF-1-Lists | yanlwsometing">
      <meta itemprop="description" content="">
    </span>
      <header class="post-header">
        <h1 class="post-title" itemprop="name headline">
          SF-1-Lists
        </h1>

        <div class="post-meta-container">
          <div class="post-meta">
    <span class="post-meta-item">
      <span class="post-meta-item-icon">
        <i class="far fa-calendar"></i>
      </span>
      <span class="post-meta-item-text">发表于</span>

      <time title="创建时间：2023-07-18 22:44:44" itemprop="dateCreated datePublished" datetime="2023-07-18T22:44:44+08:00">2023-07-18</time>
    </span>
    <span class="post-meta-item">
      <span class="post-meta-item-icon">
        <i class="far fa-calendar-check"></i>
      </span>
      <span class="post-meta-item-text">更新于</span>
      <time title="修改时间：2023-12-15 17:08:29" itemprop="dateModified" datetime="2023-12-15T17:08:29+08:00">2023-12-15</time>
    </span>
    <span class="post-meta-item">
      <span class="post-meta-item-icon">
        <i class="far fa-folder"></i>
      </span>
      <span class="post-meta-item-text">分类于</span>
        <span itemprop="about" itemscope itemtype="http://schema.org/Thing">
          <a href="/blog/categories/Coq/" itemprop="url" rel="index"><span itemprop="name">Coq</span></a>
        </span>
    </span>

  
    <span class="post-meta-item" title="阅读次数" id="busuanzi_container_page_pv">
      <span class="post-meta-item-icon">
        <i class="far fa-eye"></i>
      </span>
      <span class="post-meta-item-text">阅读次数：</span>
      <span id="busuanzi_value_page_pv"></span>
    </span>
</div>

        </div>
      </header>

    
    
    
    <div class="post-body" itemprop="articleBody"><h2 id="数值序对-Pairs-of-Numbers"><a href="#数值序对-Pairs-of-Numbers" class="headerlink" title="数值序对(Pairs of Numbers)"></a>数值序对(Pairs of Numbers)</h2><p>在 Inductive 类型定义中，每个构造子（Constructor）可以有任意多个参数 —— 可以没有（如 true 和 O），可以只有一个（如 S），也可以更多 （如 nybble，以及下文所示）。</p>
<h3 id="1-定义"><a href="#1-定义" class="headerlink" title="1. 定义"></a>1. 定义</h3><p>本文中创建了一种携带两个参数的类型，并为其声明操作函数和记法：</p>
<figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br><span class="line">3</span><br><span class="line">4</span><br><span class="line">5</span><br><span class="line">6</span><br><span class="line">7</span><br><span class="line">8</span><br><span class="line">9</span><br><span class="line">10</span><br><span class="line">11</span><br><span class="line">12</span><br><span class="line">13</span><br><span class="line">14</span><br><span class="line">15</span><br><span class="line">16</span><br><span class="line">17</span><br><span class="line">18</span><br><span class="line">19</span><br><span class="line">20</span><br><span class="line">21</span><br><span class="line">22</span><br><span class="line">23</span><br><span class="line">24</span><br><span class="line">25</span><br><span class="line">26</span><br><span class="line">27</span><br><span class="line">28</span><br><span class="line">29</span><br><span class="line">30</span><br><span class="line">31</span><br></pre></td><td class="code"><pre><span class="line">Module NatList.</span><br><span class="line"></span><br><span class="line">Inductive natprod : Type :=</span><br><span class="line">| pair (n1 n2 : nat).</span><br><span class="line"></span><br><span class="line">Definition fst (p : natprod) : nat :=</span><br><span class="line">  match p with</span><br><span class="line">  | pair x y =&gt; x</span><br><span class="line">  end.</span><br><span class="line">  </span><br><span class="line">Definition snd (p : natprod) : nat :=</span><br><span class="line">  match p with</span><br><span class="line">  | (pair x y) =&gt; y</span><br><span class="line">  end.</span><br><span class="line">  </span><br><span class="line">Notation &quot;( x , y )&quot; := (pair x y).</span><br><span class="line"></span><br><span class="line">Definition fst&#x27; (p : natprod) : nat :=</span><br><span class="line">  match p with</span><br><span class="line">  | (x,y) =&gt; x</span><br><span class="line">  end.</span><br><span class="line"></span><br><span class="line">Definition snd&#x27; (p : natprod) : nat :=</span><br><span class="line">  match p with</span><br><span class="line">  | (x,y) =&gt; y</span><br><span class="line">  end.</span><br><span class="line"></span><br><span class="line">Definition swap_pair (p : natprod) : natprod :=</span><br><span class="line">  match p with</span><br><span class="line">  | (x,y) =&gt; (y,x)</span><br><span class="line">  end.</span><br></pre></td></tr></table></figure>

<span id="more"></span>

<h3 id="2-match-p-vs-match-n-m"><a href="#2-match-p-vs-match-n-m" class="headerlink" title="2. match p vs. match n,m"></a>2. match p vs. match n,m</h3><p><strong>需要注意的是，对于natprod类型的操作函数，不要与两个变量的模式匹配混淆</strong>：</p>
<figure class="highlight ocaml"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br><span class="line">3</span><br><span class="line">4</span><br><span class="line">5</span><br><span class="line">6</span><br><span class="line">7</span><br><span class="line">8</span><br><span class="line">9</span><br><span class="line">10</span><br><span class="line">11</span><br><span class="line">12</span><br><span class="line">13</span><br></pre></td><td class="code"><pre><span class="line"><span class="comment">(* Can&#x27;t match on a pair with multiple patterns: *)</span></span><br><span class="line">       <span class="type">Definition</span> bad_fst (p : natprod) : nat :=</span><br><span class="line">         <span class="keyword">match</span> p <span class="keyword">with</span></span><br><span class="line">         | x, y =&gt; x</span><br><span class="line">         <span class="keyword">end</span>.</span><br><span class="line"></span><br><span class="line"><span class="comment">(* Can&#x27;t match on multiple values with pair patterns: *)</span></span><br><span class="line">       <span class="type">Definition</span> bad_minus (n m : nat) : nat :=</span><br><span class="line">         <span class="keyword">match</span> n, m <span class="keyword">with</span></span><br><span class="line">         | (<span class="type">O</span>   , _   ) =&gt; <span class="type">O</span></span><br><span class="line">         | (<span class="type">S</span> _ , <span class="type">O</span>   ) =&gt; n</span><br><span class="line">         | (<span class="type">S</span> n&#x27;, <span class="type">S</span> m&#x27;) =&gt; bad_minus n&#x27; m&#x27;</span><br><span class="line">         <span class="keyword">end</span>.</span><br></pre></td></tr></table></figure>

<h3 id="3-序对的简单证明"><a href="#3-序对的简单证明" class="headerlink" title="3. 序对的简单证明"></a>3. 序对的简单证明</h3><p>命题：∀ n m, (n,m) &#x3D;  (fst (n,m), snd (n,m))</p>
<p>证明：通过reflexivity简化即可 </p>
<figure class="highlight ocaml"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br><span class="line">3</span><br><span class="line">4</span><br></pre></td><td class="code"><pre><span class="line"><span class="type">Theorem</span> surjective_pairing&#x27; : forall (n m : nat),</span><br><span class="line">  (n,m) = (fst (n,m), snd (n,m)).</span><br><span class="line"><span class="type">Proof</span>.</span><br><span class="line">  reflexivity. <span class="type">Qed</span>.</span><br></pre></td></tr></table></figure>

<p>但是，将使用natprod类型再次证明却不行</p>
<figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br><span class="line">3</span><br><span class="line">4</span><br><span class="line">5</span><br></pre></td><td class="code"><pre><span class="line">Theorem surjective_pairing_stuck : forall (p : natprod),</span><br><span class="line">  p = (fst p, snd p).</span><br><span class="line">Proof.</span><br><span class="line">  simpl. (* Doesn&#x27;t reduce anything!！ *)</span><br><span class="line">Abort.</span><br></pre></td></tr></table></figure>

<p><strong>我们还需要向 Coq 展示 p 的具体结构，这样 simpl 才能对 fst 和 snd 做模式匹配。通过 destruct 可以达到这个目的。</strong></p>
<figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br><span class="line">3</span><br><span class="line">4</span><br></pre></td><td class="code"><pre><span class="line">Theorem surjective_pairing : forall (p : natprod),</span><br><span class="line">  p = (fst p, snd p).</span><br><span class="line">Proof.</span><br><span class="line">  intros p. destruct p as [n m]. simpl. reflexivity. Qed.</span><br></pre></td></tr></table></figure>

<p>注意：不同于解构自然数产生两个子目标，destruct 在此只产生 一个子目标。这是因为 natprod 只有一种构造方法。</p>
<h2 id="数值列表-Lists-of-Numbers"><a href="#数值列表-Lists-of-Numbers" class="headerlink" title="数值列表(Lists of Numbers)"></a>数值列表(Lists of Numbers)</h2><h3 id="1-定义-1"><a href="#1-定义-1" class="headerlink" title="1. 定义"></a>1. 定义</h3><p>列表类型可以如此描述：A list is either the empty list or else a pair of a number and another list.</p>
<figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br><span class="line">3</span><br><span class="line">4</span><br><span class="line">5</span><br><span class="line">6</span><br><span class="line">7</span><br><span class="line">8</span><br><span class="line">9</span><br><span class="line">10</span><br><span class="line">11</span><br></pre></td><td class="code"><pre><span class="line">Inductive natlist : Type :=</span><br><span class="line">  | nil</span><br><span class="line">  | cons (n : nat) (l : natlist).</span><br><span class="line">  </span><br><span class="line">Definition mylist := cons 1 (cons 2 (cons 3 nil)).</span><br><span class="line"></span><br><span class="line">Notation &quot;x :: l&quot; := (cons x l)</span><br><span class="line">                     (at level 60, right associativity).</span><br><span class="line">Notation &quot;[ ]&quot; := nil.</span><br><span class="line">Notation &quot;[ x ; .. ; y ]&quot; := (cons x .. (cons y nil) ..).  </span><br><span class="line"></span><br></pre></td></tr></table></figure>

<p>操作函数</p>
<figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br><span class="line">3</span><br><span class="line">4</span><br><span class="line">5</span><br><span class="line">6</span><br><span class="line">7</span><br><span class="line">8</span><br><span class="line">9</span><br><span class="line">10</span><br><span class="line">11</span><br><span class="line">12</span><br><span class="line">13</span><br><span class="line">14</span><br><span class="line">15</span><br><span class="line">16</span><br><span class="line">17</span><br><span class="line">18</span><br><span class="line">19</span><br><span class="line">20</span><br><span class="line">21</span><br><span class="line">22</span><br><span class="line">23</span><br><span class="line">24</span><br><span class="line">25</span><br><span class="line">26</span><br><span class="line">27</span><br><span class="line">28</span><br><span class="line">29</span><br><span class="line">30</span><br><span class="line">31</span><br><span class="line">32</span><br><span class="line">33</span><br><span class="line">34</span><br><span class="line">35</span><br><span class="line">36</span><br><span class="line">37</span><br><span class="line">38</span><br></pre></td><td class="code"><pre><span class="line">(** *** Repeat *)</span><br><span class="line">(** Next let&#x27;s look at several functions for constructing and</span><br><span class="line">    manipulating lists.  First, the [repeat] function takes a number</span><br><span class="line">    [n] and a [count] and returns a list of length [count] in which</span><br><span class="line">    every element is [n]. *)</span><br><span class="line"></span><br><span class="line">Fixpoint repeat (n count : nat) : natlist :=</span><br><span class="line">  match count with</span><br><span class="line">  | O =&gt; nil</span><br><span class="line">  | S count&#x27; =&gt; n :: (repeat n count&#x27;)</span><br><span class="line">  end.</span><br><span class="line"></span><br><span class="line">(** *** Length *)</span><br><span class="line">(** The [length] function calculates the length of a list. *)</span><br><span class="line"></span><br><span class="line">Fixpoint length (l:natlist) : nat :=</span><br><span class="line">  match l with</span><br><span class="line">  | nil =&gt; O</span><br><span class="line">  | h :: t =&gt; S (length t)</span><br><span class="line">  end.</span><br><span class="line"></span><br><span class="line">(** *** Append *)</span><br><span class="line">(** The [app] function concatenates (appends) two lists. *)</span><br><span class="line"></span><br><span class="line">Fixpoint app (l1 l2 : natlist) : natlist :=</span><br><span class="line">  match l1 with</span><br><span class="line">  | nil =&gt; l2</span><br><span class="line">  | h :: t =&gt; h :: (app t l2)</span><br><span class="line">  end.</span><br><span class="line"></span><br><span class="line">Notation &quot;x ++ y&quot; := (app x y)</span><br><span class="line">                     (right associativity, at level 60).</span><br><span class="line">Example test_app1: [1;2;3] ++ [4;5] = [1;2;3;4;5].</span><br><span class="line">Proof. reflexivity. Qed.</span><br><span class="line">Example test_app2: nil ++ [4;5] = [4;5].</span><br><span class="line">Proof. reflexivity. Qed.</span><br><span class="line">Example test_app3: [1;2;3] ++ nil = [1;2;3].</span><br><span class="line">Proof. reflexivity. Qed.</span><br></pre></td></tr></table></figure>

<h3 id="2-用列表实现口袋（Bag）"><a href="#2-用列表实现口袋（Bag）" class="headerlink" title="2. 用列表实现口袋（Bag）"></a>2. 用列表实现口袋（Bag）</h3><p>bag（或者叫 multiset 多重集）类似于集合，只是其中每个元素都能出现不止一次。 口袋的一种可行的表示是列表。</p>
<figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br></pre></td><td class="code"><pre><span class="line">Definition bag := natlist.</span><br></pre></td></tr></table></figure>

<p>对于其操作的函数</p>
<figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br><span class="line">3</span><br><span class="line">4</span><br><span class="line">5</span><br><span class="line">6</span><br><span class="line">7</span><br><span class="line">8</span><br><span class="line">9</span><br><span class="line">10</span><br><span class="line">11</span><br><span class="line">12</span><br><span class="line">13</span><br><span class="line">14</span><br><span class="line">15</span><br><span class="line">16</span><br><span class="line">17</span><br><span class="line">18</span><br><span class="line">19</span><br><span class="line">20</span><br><span class="line">21</span><br><span class="line">22</span><br><span class="line">23</span><br><span class="line">24</span><br><span class="line">25</span><br><span class="line">26</span><br><span class="line">27</span><br><span class="line">28</span><br><span class="line">29</span><br><span class="line">30</span><br><span class="line">31</span><br><span class="line">32</span><br><span class="line">33</span><br><span class="line">34</span><br><span class="line">35</span><br><span class="line">36</span><br><span class="line">37</span><br></pre></td><td class="code"><pre><span class="line">Fixpoint count (v : nat) (s : bag) : nat :=</span><br><span class="line">  match s with </span><br><span class="line">  | nil =&gt; 0</span><br><span class="line">  | h :: t =&gt; if eqb h v then S (count v t)</span><br><span class="line">              else count v t</span><br><span class="line">  end.</span><br><span class="line">  </span><br><span class="line">Definition add (v : nat) (s : bag) : bag :=</span><br><span class="line">  v :: s.</span><br><span class="line">  </span><br><span class="line">Fixpoint member (v : nat) (s : bag) : bool :=</span><br><span class="line">  match s with</span><br><span class="line">  | nil =&gt; false</span><br><span class="line">  | h :: t =&gt; if eqb v h then true</span><br><span class="line">              else member v t</span><br><span class="line">  end.</span><br><span class="line">  </span><br><span class="line">Fixpoint remove_one (v : nat) (s : bag) : bag :=</span><br><span class="line">  match s with</span><br><span class="line">  | nil =&gt; nil</span><br><span class="line">  | h :: t =&gt; if eqb v h then t</span><br><span class="line">              else h :: remove_one v t</span><br><span class="line">  end.</span><br><span class="line">Fixpoint remove_all (v:nat) (s:bag) : bag :=</span><br><span class="line">   match s with</span><br><span class="line">  | nil =&gt; nil</span><br><span class="line">  | h :: t =&gt; if eqb v h then remove_all v t</span><br><span class="line">              else h :: remove_all v t</span><br><span class="line">  end.</span><br><span class="line">Fixpoint included (s1 : bag) (s2 : bag) : bool :=</span><br><span class="line">  match s1 with</span><br><span class="line">  | nil =&gt; true</span><br><span class="line">  | h :: t =&gt; match member h s2 with</span><br><span class="line">              | true =&gt; included t (remove_one h s2)</span><br><span class="line">              | false =&gt; false</span><br><span class="line">              end</span><br><span class="line">  end.</span><br></pre></td></tr></table></figure>

<h2 id="有关列表的论证-Reasoning-About-Lists"><a href="#有关列表的论证-Reasoning-About-Lists" class="headerlink" title="有关列表的论证(Reasoning About Lists)"></a>有关列表的论证(Reasoning About Lists)</h2><p>对于列表的简单事实，可以通过*化简(Simplification)<em>和</em>分类(destruct)*解决</p>
<figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br><span class="line">3</span><br><span class="line">4</span><br><span class="line">5</span><br><span class="line">6</span><br><span class="line">7</span><br><span class="line">8</span><br><span class="line">9</span><br><span class="line">10</span><br><span class="line">11</span><br><span class="line">12</span><br></pre></td><td class="code"><pre><span class="line">Theorem nil_app : forall l:natlist,</span><br><span class="line">  [] ++ l = l.</span><br><span class="line">Proof. reflexivity. Qed.</span><br><span class="line"></span><br><span class="line">Theorem tl_length_pred : forall l:natlist,</span><br><span class="line">  pred (length l) = length (tl l).</span><br><span class="line">Proof.</span><br><span class="line">  intros l. destruct l as [| n l&#x27;].</span><br><span class="line">  - (* l = nil *)</span><br><span class="line">    reflexivity.</span><br><span class="line">  - (* l = cons n l&#x27; *)</span><br><span class="line">    reflexivity. Qed.</span><br></pre></td></tr></table></figure>

<h3 id="1-对列表归纳-Induction-on-Lists"><a href="#1-对列表归纳-Induction-on-Lists" class="headerlink" title="1. 对列表归纳(Induction on Lists)"></a>1. 对列表归纳(Induction on Lists)</h3><p>对比对自然数的归纳，归纳证明 natlist 这样的数据类型也是类似的。如果我们有某个命题 P 涉及列表 l，而我们想证明 P 对 ‘一切’ 列表都成立，那么可以像这样推理：</p>
<ul>
<li>首先，证明当 l 为 nil 时 P l 成立。</li>
<li>然后，证明当 l 为 cons n l’ 时 P l 成立，其中 n 是某个自然数，l’ 是某个更小的列表，假设 P l’ 成立.</li>
</ul>
<figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br><span class="line">3</span><br><span class="line">4</span><br><span class="line">5</span><br><span class="line">6</span><br><span class="line">7</span><br><span class="line">8</span><br><span class="line">9</span><br><span class="line">10</span><br></pre></td><td class="code"><pre><span class="line">Theorem app_assoc : forall l1 l2 l3 : natlist,</span><br><span class="line">  (l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3).</span><br><span class="line">Proof.</span><br><span class="line">  intros l1 l2 l3. </span><br><span class="line">  induction l1 as [| n l1&#x27; IHl1&#x27;].</span><br><span class="line">  - (* l1 = nil *)</span><br><span class="line">    reflexivity.</span><br><span class="line">  - (* l1 = cons n l1&#x27; *)</span><br><span class="line">    simpl. rewrite -&gt; IHl1&#x27;. reflexivity. </span><br><span class="line">Qed.</span><br></pre></td></tr></table></figure>

<p>形式化证明：</p>
<p>‘定理’：对所有的列表 l1, l2, 和 l3， (l1 ++ l2) ++ l3 &#x3D; l1 ++ (l2 ++ l3)。<br>‘证明’: 通过对 l1 使用归纳法。<br>首先, 假设 l1 &#x3D; []。我们必须证明：<br>       ([] ++ l2) ++ l3 &#x3D; [] ++ (l2 ++ l3),<br>这可以通过展开 ++ 的定义得到。<br>然后, 假设 l1 &#x3D; n::l1’，有：<br>       (l1’ ++ l2) ++ l3 &#x3D; l1’ ++ (l2 ++ l3)<br>（归纳假设）。我们必须证明：<br>       ((n :: l1’) ++ l2) ++ l3 &#x3D; (n :: l1’) ++ (l2 ++ l3).<br>根据 ++ 的定义, 上式等价于：<br>       n :: ((l1’ ++ l2) ++ l3) &#x3D; n :: (l1’ ++ (l2 ++ l3)),<br>该式可通过我们的归纳假设立即证得</p>
<h3 id="2-反转列表-Reversing-a-List"><a href="#2-反转列表-Reversing-a-List" class="headerlink" title="2. 反转列表(Reversing a List )"></a>2. 反转列表(Reversing a List )</h3><p>定义一个列表反转函数 rev：</p>
<figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br><span class="line">3</span><br><span class="line">4</span><br><span class="line">5</span><br><span class="line">6</span><br><span class="line">7</span><br><span class="line">8</span><br><span class="line">9</span><br><span class="line">10</span><br></pre></td><td class="code"><pre><span class="line">Fixpoint rev (l:natlist) : natlist :=</span><br><span class="line">  match l with</span><br><span class="line">  | nil ⇒ nil</span><br><span class="line">  | h :: t ⇒ rev t ++ [h]</span><br><span class="line">  end.</span><br><span class="line"> </span><br><span class="line">Example test_rev1: rev [1;2;3] = [3;2;1].</span><br><span class="line">Proof. reflexivity. Qed.</span><br><span class="line">Example test_rev2: rev nil = nil.</span><br><span class="line">Proof. reflexivity. Qed.</span><br></pre></td></tr></table></figure>

<p>证明反转一个列表不会改变它的长度</p>
<figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br><span class="line">3</span><br><span class="line">4</span><br><span class="line">5</span><br><span class="line">6</span><br><span class="line">7</span><br><span class="line">8</span><br><span class="line">9</span><br><span class="line">10</span><br><span class="line">11</span><br><span class="line">12</span><br><span class="line">13</span><br><span class="line">14</span><br><span class="line">15</span><br><span class="line">16</span><br><span class="line">17</span><br><span class="line">18</span><br><span class="line">19</span><br><span class="line">20</span><br></pre></td><td class="code"><pre><span class="line">Theorem app_length : forall l1 l2 : natlist,</span><br><span class="line">  length (l1 ++ l2) = (length l1) + (length l2).</span><br><span class="line">Proof.</span><br><span class="line">  (* 课上已完成 *)</span><br><span class="line">  intros l1 l2. induction l1 as [| n l1&#x27; IHl1&#x27;].</span><br><span class="line">  - (* l1 = nil *)</span><br><span class="line">    reflexivity.</span><br><span class="line">  - (* l1 = cons *)</span><br><span class="line">    simpl. rewrite -&gt; IHl1&#x27;. reflexivity. Qed.</span><br><span class="line"></span><br><span class="line">Theorem rev_length_firsttry : forall l : natlist,</span><br><span class="line">  length (rev l) = length l.</span><br><span class="line">Proof.</span><br><span class="line">  intros l. induction l as [ | n l&#x27; IHl&#x27;].</span><br><span class="line">  - simpl. reflexivity.</span><br><span class="line">  - simpl.  rewrite -&gt; app_length. </span><br><span class="line">    simpl. rewrite -&gt; IHl&#x27;. </span><br><span class="line">    rewrite add_comm.  reflexivity.</span><br><span class="line">Qed.</span><br><span class="line"></span><br></pre></td></tr></table></figure>

<p>‘定理’: 对于所有的列表 l，length (rev l) &#x3D; length l。<br>‘证明’: 对 l 进行归纳。<br>首先，假设 l &#x3D; []。我们必须证明<br>          length (rev []) &#x3D; length [],<br>根据 length 和 rev 的定义，上式显然可得。<br>其次，假设 l &#x3D; n::l’，并且<br>          length (rev l’) &#x3D; length l’.<br>我们必须证明<br>          length (rev (n :: l’)) &#x3D; length (n :: l’).<br>根据 rev 的定义，上式来自于<br>          length ((rev l’) ++ [n]) &#x3D; S (length l’)<br>根据之前的引理，此式等同于<br>          length (rev l’) + length [n] &#x3D; S (length l’).<br>根据归纳假设和 length 的定义，上式显然可得。</p>
<h3 id="3-Search"><a href="#3-Search" class="headerlink" title="3.  Search"></a>3.  Search</h3><p>在Coq中，你可以使用 <code>Search</code> 命令来搜索与给定的模式匹配的标识符、假设或引理。<code>Search</code> 命令可以帮助你找到与你的目标或问题相关的定义、引理或定理。</p>
<p><code>Search</code> 命令的语法如下：<code>Search pattern.</code>。其中，<code>pattern</code> 是你要搜索的模式。模式可以是标识符、表达式、引理语句等。</p>
<p>以下是几个示例，展示了 <code>Search</code> 命令的使用方法：</p>
<ul>
<li><p>搜索某个标识符：</p>
<figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br></pre></td><td class="code"><pre><span class="line">Search plus.</span><br></pre></td></tr></table></figure>

<p>这会搜索包含关键词 “plus” 的标识符，如 <code>Nat.add</code>、<code>Nat.add_0_r</code> 等（add涉及到plus函数）。</p>
</li>
<li><p>搜索某个已知的引理或定理：</p>
<figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br></pre></td><td class="code"><pre><span class="line">Search (_ + _ = _ + _).</span><br></pre></td></tr></table></figure>

<p>这会搜索形式类似于 <code>_ + _ = _ + _</code> 的引理或定理，例如 <code>Nat.add_comm</code>、<code>Nat.add_assoc</code> 等。</p>
</li>
<li><p>搜索特定类型的假设：</p>
<figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br></pre></td><td class="code"><pre><span class="line">Search (forall (_ : nat), _ = _ -&gt; _ = _).</span><br></pre></td></tr></table></figure>

<p>这会搜索具有形式 <code>forall (_ : nat), _ = _ -&gt; _ = _</code> 的假设，其中 <code>_</code> 用于匹配任意的项。</p>
</li>
<li><p>在某个模块中搜索</p>
<figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br></pre></td><td class="code"><pre><span class="line">Search (_ + _ = _ + _) inside Induction.</span><br></pre></td></tr></table></figure></li>
</ul>
<p>需要注意的是，<code>Search</code> 命令会搜索当前环境中可见的定义和引理。如果你在证明中使用了 <code>Require</code> 或 <code>Import</code> 命令导入了其他模块，那么 <code>Search</code> 命令也会搜索这些导入的模块中的定义和引理。</p>
<h2 id="Options-可选类型"><a href="#Options-可选类型" class="headerlink" title="Options 可选类型"></a>Options 可选类型</h2><p>假设我们想要写一个返回某个列表中第 n 个元素的函数。如果我们为它赋予类型 nat → natlist → nat，那么当列表太短时我们仍须返回某个数…</p>
<figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br><span class="line">3</span><br><span class="line">4</span><br><span class="line">5</span><br><span class="line">6</span><br><span class="line">7</span><br><span class="line">8</span><br></pre></td><td class="code"><pre><span class="line">Fixpoint nth_bad (l:natlist) (n:nat) : nat :=</span><br><span class="line">  match l with</span><br><span class="line">  | nil =&gt; 42</span><br><span class="line">  | a :: l&#x27; =&gt; match n with</span><br><span class="line">               | 0 =&gt; a</span><br><span class="line">               | S n&#x27; =&gt; nth_bad l&#x27; n&#x27;</span><br><span class="line">               end</span><br><span class="line">  end.</span><br></pre></td></tr></table></figure>

<p>但是，这样会产生混淆，因此需要改变 nth_bad 的返回类型，使其包含一个错误值作为可能的结果。 我们将此类型命名为 natoption</p>
<figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br><span class="line">3</span><br></pre></td><td class="code"><pre><span class="line">Inductive natoption : Type :=</span><br><span class="line">  | Some (n : nat)</span><br><span class="line">  | None.</span><br></pre></td></tr></table></figure>



<h2 id="偏映射-（Partial-Maps）"><a href="#偏映射-（Partial-Maps）" class="headerlink" title="偏映射 （Partial Maps）"></a>偏映射 （Partial Maps）</h2><p>这是一个简单的 <em>‘偏映射’</em> 数据类型，它类似于大多数编程语言中的映射或字典数据结构。</p>
<figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br><span class="line">3</span><br><span class="line">4</span><br><span class="line">5</span><br><span class="line">6</span><br><span class="line">7</span><br></pre></td><td class="code"><pre><span class="line">Inductive id : Type :=</span><br><span class="line">  | Id (n : nat).</span><br><span class="line">  </span><br><span class="line">Inductive partial_map : Type :=</span><br><span class="line">  | empty</span><br><span class="line">  | record (i : id) (v : nat) (m : partial_map).</span><br><span class="line">  </span><br></pre></td></tr></table></figure>

<h2 id="Exercises"><a href="#Exercises" class="headerlink" title="Exercises"></a>Exercises</h2><ol>
<li>Exercise: 3 stars, advanced (alternate)：设计一个函数，将两个列表交替合并 <figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br><span class="line">3</span><br><span class="line">4</span><br><span class="line">5</span><br><span class="line">6</span><br><span class="line">7</span><br><span class="line">8</span><br><span class="line">9</span><br><span class="line">10</span><br><span class="line">11</span><br><span class="line">12</span><br><span class="line">13</span><br><span class="line">14</span><br><span class="line">15</span><br><span class="line">16</span><br><span class="line">17</span><br><span class="line">18</span><br><span class="line">19</span><br><span class="line">20</span><br><span class="line">21</span><br><span class="line">22</span><br><span class="line">23</span><br></pre></td><td class="code"><pre><span class="line"></span><br><span class="line"></span><br><span class="line">Fixpoint alternate (l1 l2 : natlist) : natlist :=</span><br><span class="line">  match l1 with</span><br><span class="line">  | nil =&gt; l2</span><br><span class="line">  | h1 :: t1 =&gt; h1 :: match l2 with</span><br><span class="line">              | nil =&gt; t1</span><br><span class="line">              | h2 :: t2 =&gt; h2 :: alternate t1 t2</span><br><span class="line">              end</span><br><span class="line">  end.</span><br><span class="line">  </span><br><span class="line">Example test_alternate1:</span><br><span class="line">  alternate [1;2;3] [4;5;6] = [1;4;2;5;3;6].</span><br><span class="line">  (* FILL IN HERE *) Admitted.</span><br><span class="line">Example test_alternate2:</span><br><span class="line">  alternate [1] [4;5;6] = [1;4;5;6].</span><br><span class="line">  (* FILL IN HERE *) Admitted.</span><br><span class="line">Example test_alternate3:</span><br><span class="line">  alternate [1;2;3] [4] = [1;4;2;3].</span><br><span class="line">  (* FILL IN HERE *) Admitted.</span><br><span class="line">Example test_alternate4:</span><br><span class="line">  alternate [] [20;30] = [20;30].</span><br><span class="line">  (* FILL IN HERE *) Admitted.</span><br></pre></td></tr></table></figure></li>
</ol>

    </div>

    
    
    

    <footer class="post-footer">

        

          <div class="post-nav">
            <div class="post-nav-item">
                <a href="/blog/2023/06/30/Linux%EF%BC%88%E4%BA%8C%EF%BC%89/" rel="prev" title="Linux（二）">
                  <i class="fa fa-chevron-left"></i> Linux（二）
                </a>
            </div>
            <div class="post-nav-item">
                <a href="/blog/2023/07/19/SF-1-Poly/" rel="next" title="SF-1-Poly">
                  SF-1-Poly <i class="fa fa-chevron-right"></i>
                </a>
            </div>
          </div>
    </footer>
  </article>
</div>






</div>
  </main>

  <footer class="footer">
    <div class="footer-inner">


<div class="copyright">
  &copy; 
  <span itemprop="copyrightYear">2023</span>
  <span class="with-love">
    <i class="fa fa-heart"></i>
  </span>
  <span class="author" itemprop="copyrightHolder">yanlw</span>
</div>
<div class="busuanzi-count">
    <span class="post-meta-item" id="busuanzi_container_site_uv">
      <span class="post-meta-item-icon">
        <i class="fa fa-user"></i>
      </span>
      <span class="site-uv" title="总访客量">
        <span id="busuanzi_value_site_uv"></span>
      </span>
    </span>
    <span class="post-meta-item" id="busuanzi_container_site_pv">
      <span class="post-meta-item-icon">
        <i class="fa fa-eye"></i>
      </span>
      <span class="site-pv" title="总访问量">
        <span id="busuanzi_value_site_pv"></span>
      </span>
    </span>
</div>
  <div class="powered-by">由 <a href="https://hexo.io/" rel="noopener" target="_blank">Hexo</a> & <a href="https://theme-next.js.org/pisces/" rel="noopener" target="_blank">NexT.Pisces</a> 强力驱动
  </div>

    </div>
  </footer>

  
  <div class="reading-progress-bar"></div>

  <a href="https://gitee.com/yanlwsometing" class="github-corner" title="在 GitHub 上关注我" aria-label="在 GitHub 上关注我" rel="noopener" target="_blank"><svg width="80" height="80" viewBox="0 0 250 250" aria-hidden="true"><path d="M0,0 L115,115 L130,115 L142,142 L250,250 L250,0 Z"></path><path d="M128.3,109.0 C113.8,99.7 119.0,89.6 119.0,89.6 C122.0,82.7 120.5,78.6 120.5,78.6 C119.2,72.0 123.4,76.3 123.4,76.3 C127.3,80.9 125.5,87.3 125.5,87.3 C122.9,97.6 130.6,101.9 134.4,103.2" fill="currentColor" style="transform-origin: 130px 106px;" class="octo-arm"></path><path d="M115.0,115.0 C114.9,115.1 118.7,116.5 119.8,115.4 L133.7,101.6 C136.9,99.2 139.9,98.4 142.2,98.6 C133.8,88.0 127.5,74.4 143.8,58.0 C148.5,53.4 154.0,51.2 159.7,51.0 C160.3,49.4 163.2,43.6 171.4,40.1 C171.4,40.1 176.1,42.5 178.8,56.2 C183.1,58.6 187.2,61.8 190.9,65.4 C194.5,69.0 197.7,73.2 200.1,77.6 C213.8,80.2 216.3,84.9 216.3,84.9 C212.7,93.1 206.9,96.0 205.4,96.6 C205.1,102.4 203.0,107.8 198.3,112.5 C181.9,128.9 168.3,122.5 157.7,114.1 C157.9,116.9 156.7,120.9 152.7,124.9 L141.0,136.5 C139.8,137.7 141.6,141.9 141.8,141.8 Z" fill="currentColor" class="octo-body"></path></svg></a>

<noscript>
  <div class="noscript-warning">Theme NexT works best with JavaScript enabled</div>
</noscript>


  
  <script src="https://cdnjs.cloudflare.com/ajax/libs/animejs/3.2.1/anime.min.js" integrity="sha256-XL2inqUJaslATFnHdJOi9GfQ60on8Wx1C2H8DYiN1xY=" crossorigin="anonymous"></script>
  <script src="https://cdnjs.cloudflare.com/ajax/libs/jquery/3.6.4/jquery.min.js" integrity="sha256-oP6HI9z1XaZNBrJURtCoUT5SUnxFr8s3BzRl+cbzUq8=" crossorigin="anonymous"></script>
  <script src="https://cdnjs.cloudflare.com/ajax/libs/fancybox/3.5.7/jquery.fancybox.min.js" integrity="sha256-yt2kYMy0w8AbtF89WXb2P1rfjcP/HTHLT7097U8Y5b8=" crossorigin="anonymous"></script>
<script src="/blog/js/comments.js"></script><script src="/blog/js/utils.js"></script><script src="/blog/js/next-boot.js"></script>

  


  <script src="/blog/js/third-party/fancybox.js"></script>



  
  <script async src="https://busuanzi.ibruce.info/busuanzi/2.3/busuanzi.pure.mini.js"></script>





</body>
</html>
